$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, $P$:(\{$e$:es{-}E(${\it es}$)$\mid$ loc($e$) = $i$\} $\rightarrow$prop\{i:l\}).
\\[0ex]alle{-}at(${\it es}$; $i$; $e$.$P$($e$)) $\in$ prop\{i:l\}